feat(alias_elimination): detect x ~ -y perfect aliases#4540
Conversation
I think for the 0 case it's worth including sticky non-irreducible variables too (i.e. ones with positive state priority). The variable cannot possibly be anything else, so it serves no purpose participating in state selection. Substituting zeros into other equations may also simplify them drastically. Knowing something is zero is very useful information. |
|
Good point. Irreducible can just leave the variable with the equation x~0. |
I've actually gone a step further and have included irreducibles as well in this. Just because we are irreducible doesn't mean we can't substitute away all users. We now make irreducibles remain as |
AayushSabharwal
left a comment
AayushSabharwal
left a comment
There was a problem hiding this comment.
I just realized, if we eliminate a variable as zero and substitute the zero into other equations, we have to update the incidence of those equations.
Is this just for cases where we have Edit: this is wrong. there's lots of nonlinear cases as well. |
|
Should be fixed. |
|
@AayushSabharwal can you have another look at this? |
|
|
|
Congratulations! You uncovered a bug in |
Extend `find_perfect_aliases!` to recognize the negated alias pattern `c1*v1 + c2*v2 ~ 0` with `c1 == c2` (i.e. `x ~ -y`) in addition to the existing `c1 == -c2` case (`x ~ y`). Each candidate alias edge carries an `Int8` sign, and a BFS from each group's chosen target propagates signs to every member -- so transitive chains including double negation (`x ~ -y` and `y ~ -z` ⇒ `x ~ z`) are resolved correctly. When a group's signed edges are inconsistent (e.g. `x ~ y` and `x ~ -y` both appear), every non-sticky variable in that group is substituted with `0` and a `v ~ 0` equation is added to `additional_observed`; irreducibles remain unknowns and the surviving alias equations carry the resulting `irr ~ 0` constraint into the system. Substitution rhs and derivative-cascade substitutions both honor the propagated sign. Tests cover: basic `y ~ -x`, mixed chain `x ~ y, y ~ -z`, double-negation transitivity, negated alias with irreducible target, and the sign-conflict force-to-zero case. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Split the loop over `candidate_eqs` into separate conflict-group and
consistent-group passes. The conflict-group pass now eagerly pins one
irreducible per claimed alias equation by rewriting it to `v ~ 0` (and
stripping the bipartite edge to the other endpoint), which both:
- correctly handles the previously-incorrect case where both
endpoints of a conflict-group alias equation are irreducible (the
surviving `c1*v1 + c2*v2 = 0` did not individually pin either to
zero), and
- eliminates the need for a separate `pinned_eqs` data structure
living across the substitution pass.
The main alias_sets loop now only needs to distinguish "irreducible in
a conflict group" (just mark `always_present`, since the pin is already
written) from non-irreducibles (substitute to 0 / to ±target as
before). Priority>0 non-irreducibles in conflict groups are eliminated
normally instead of being kept as unconstrained unknowns.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Switch the negated-alias testset from `@mtkcompile` to `TearingState` + `eliminate_perfect_aliases!` so we verify the behavior of this pass in isolation rather than the cumulative output of `mtkcompile`. Assertions now target `state.additional_observed`, `equations(state.sys)`, `state.fullvars`, and `state.always_present`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Aayush Sabharwal <aayush.sabharwal@gmail.com>
Co-authored-by: Aayush Sabharwal <aayush.sabharwal@gmail.com>
Co-authored-by: Aayush Sabharwal <aayush.sabharwal@gmail.com>
Co-authored-by: Aayush Sabharwal <aayush.sabharwal@gmail.com>
Co-authored-by: Aayush Sabharwal <aayush.sabharwal@gmail.com>
oscardssmith
force-pushed
the
os/detect-negative-perfect-aliases
branch
from
da4b96a to
60ad3fe
Compare
|
rebased. |
|
🎉 |
3 participants
Extend
find_perfect_aliases!to recognize the negated alias patternc1*v1 + c2*v2 ~ 0withc1 == c2(i.e.x ~ -y) in addition to the existingc1 == -c2case (x ~ y). Each candidate alias edge carries anInt8sign, and a BFS from each group's chosen target propagates signs to every member -- so transitive chains including double negation (x ~ -yandy ~ -z⇒x ~ z) are resolved correctly.When a group's signed edges are inconsistent (e.g.
x ~ yandx ~ -yboth appear), every non-sticky variable in that group is substituted with0and av ~ 0equation is added toadditional_observed; irreducibles remain unknowns and the surviving alias equations carry the resultingirr ~ 0constraint into the system. Substitution rhs and derivative-cascade substitutions both honor the propagated sign.Tests cover: basic
y ~ -x, mixed chainx ~ y, y ~ -z, double-negation transitivity, negated alias with irreducible target, and the sign-conflict force-to-zero case.Claude wrote most of this, but it seems pretty reasonably implemented.